Knowledge compilation is an approach to tackle the computationalintractability of general reasoning problems. According to this approach,knowledge bases are converted off-line into a target compilation language whichis tractable for on-line querying. Reduced ordered binary decision diagram(ROBDD) is one of the most influential target languages. We generalize ROBDD byassociating some implied literals in each node and the new language is calledreduced ordered binary decision diagram with implied literals (ROBDD-L). Thenwe discuss a kind of subsets of ROBDD-L called ROBDD-i with precisely i impliedliterals (0 \leq i \leq \infty). In particular, ROBDD-0 is isomorphic to ROBDD;ROBDD-\infty requires that each node should be associated by the impliedliterals as many as possible. We show that ROBDD-i has uniqueness over somespecific variables order, and ROBDD-\infty is the most succinct subset inROBDD-L and can meet most of the querying requirements involved in theknowledge compilation map. Finally, we propose an ROBDD-i compilation algorithmfor any i and a ROBDD-\infty compilation algorithm. Based on them, we implementa ROBDD-L package called BDDjLu and then get some conclusions from preliminaryexperimental results: ROBDD-\infty is obviously smaller than ROBDD for allbenchmarks; ROBDD-\infty is smaller than the d-DNNF the benchmarks whosecompilation results are relatively small; it seems that it is better totransform ROBDDs-\infty into FBDDs and ROBDDs rather than straight compile thebenchmarks.
展开▼